
/* Bidder1 States */

mtype = {idleB, startB, submittedB, lost, won};

/* Auctioneer States */

mtype ={waitA, startA, processBidA, endA};

/* Events*/

mtype = {start_auction, auction_started, status, winner, end_auction, dummy};

mtype stateB;
mtype stateA;
mtype stateWinner;

/* channels for transitions */	

chan m2A = [0] of {int, mtype};
chan m2B = [0] of {int, mtype};
int clientBid;
int startBid=13; 

init {
    atomic {
        if
        :: skip -> clientBid = 12;
        :: skip -> clientBid = 13;
        :: skip -> clientBid = 14;
        fi;
    }
    run auctioneer();
    m2A!0, start_auction;
    printf("Msg to start the auction\n");
}

/*Client process*/

proctype client1() {
    stateB = idleB;
    
    do
    :: (stateB == idleB) -> printf("Client waiting for auction to start\n");
        if
        :: m2B?0, auction_started->
            printf("The auction is now open, the client knows");
            stateB = startB;
        :: m2B?0, end_auction -> printf("Auction is terminating \n");
            break;
        fi;
    :: (stateB == startB) -> printf("Ready to submit a bid\n");
        printf("Sending bid %d\n",clientBid);
        m2A!clientBid, dummy;
        stateB = submittedB;
    ::(stateB == submittedB) -> printf("Bid submitted\n");
        printf("Waiting for the result now\n");
        if
        ::m2B?0, status ->
            printf("Bid too low\n");
            stateB = idleB;
            stateWinner = lost; 
        ::m2B?0, winner->
            printf("Hurray, I won\n");
            stateB=idleB;
            clientBid=0;
            stateWinner = won;
        fi;
    od;
}


/*Auction process*/

proctype auctioneer() {
    stateA = waitA;
    run client1();
    do
    :: (stateA == waitA) -> printf("Waiting to start the auction\n");
        m2A?0, start_auction;
        printf("Ready to get the auction started\n");
        m2B!0, auction_started;
        stateA= startA;
        printf("Sending start signal\n");
    :: (stateA == startA) -> printf("Waiting for a bid to be submitted....\n");
        m2A?clientBid, dummy; 
        printf("Client bid received\n");
        stateA=processBidA;
    :: (stateA == processBidA) -> printf("Computing current winner\n");
        if
        :: clientBid>=startBid -> m2B!0, winner;stateA=endA;
        :: clientBid<startBid -> m2B!0, status;stateA = endA; 
        fi;
    :: (stateA == endA) -> printf("Winner elected.Auction will terminate\n");
        m2B!0,end_auction;
        break;
    od;
}

ltl test {(<>(clientBid>=startBid) -> <>(stateWinner==won))}
